$\vdash$  $\forall$$T$:Type, $A$:$\mathbb{P}$, $B$:($T$$\rightarrow\mathbb{P}$). ($\exists$$x$:$T$. ($A$ \& $B$($x$))) $\Leftarrow\!\Rightarrow$ ($A$ \& ($\exists$$x$:$T$. $B$($x$)))